the_w:World, e:E, t:.
FairFifo
 isrcv(kind(e))
 match(lnk(kind(e));t;time(e))
 (msg(a(loc(e);time(e)))  onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))) 

latex

Definitions

||as||, -n, n+m, time(e), n-m, Msg, (x  l), P  Q, False, A, AB, P & Q, i  j < k, {x:A| B(x) }, , {i..j}, t  T, #$n, x:A. B(x), x:AB(x), <a,b>, {T}, SQType(T), Prop, s ~ t, x:AB(x), A & B, x:A. B(x), World, E, FairFifo, kind(e), isrcv(k), b, lnk(k), match(l;t;t'), , s = t, a<b, snds(l;t), rcvs(l;t), destination(l), Action(i), Void, m(i;t), onlnk(l;mss), source(l), w.M, mlnk(m), Id, Msg(M), type List, S  T, l[i], Type, IdLnk

Lemmas

select wf, w-onlnk wf, w-m wf, Msg wf, Id wf, mlnk wf, w-M wf, lsrc wf, w-action wf, ldst wf, w-rcvs wf, length wf1, w-Msg wf, w-snds wf, w-match wf, lnk wf, w-time wf, assert wf, isrcv wf, w-ekind wf, fair-fifo wf, nat wf, w-E wf, world wf, better-w-match-exists, w-match-unique, le wf